COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	heavy[e86,jmc]	Heavy duty set theory
C00003 ENDMK
C⊗;
heavy[e86,jmc]	Heavy duty set theory

	It is hard to determine exactly what should be in it.  However,
we can get a clue by demanding that certain arguments be obvious or
at least very brief.

1. card{a,b,c,d,e, ... ,z} = 26 should lead readily to c ≠ j.
Maybe this is just a matter of syntactic programmability in the proof-checker,
because it should be immediate that c=i ⊃ card{a,b,d,...,i,k,...,z} ≥ 25,
hence card{b,d etc.} ≥ 24 and so on to card{} ≥ 1 which is false.